Nuprl Lemma : seq-count_wf
0,22
postcript
pdf
T
:Type,
eq
:(
T
T
),
f
:(
T
),
x
:
T
,
j
:
. #{i<
j
|
f
i
eq
x
}
(
j
+1)
latex
Definitions
Type
,
t
T
,
,
x
:
A
B
(
x
)
,
,
{
x
:
A
|
B
(
x
) }
,
x
:
A
.
B
(
x
)
,
#$n
,
{
i
..
j
}
,
A
B
,
S
T
,
P
&
Q
,
i
j
<
k
,
S
T
,
f
(
a
)
,
f
o
g
,
size(
k
;
f
)
,
#{i<
j
|
f
i
eq
x
}
Lemmas
bool-size
wf
,
compose
wf
,
le
wf
,
int
seg
wf
,
nat
wf
,
bool
wf
origin
T:Type, eq:(T
T
), f:(
T), x:T, j:. #{i<j|f i eq x} 
(j+1) T:Type, eq:(TT), f:(T), x:T, j:. #{i<j|f i eq x} (j+1) TB(x)x:A. B(x)
}
B
T j < k
Tsize(k;f)